%Consigna: Modifica al gateway g luego de procesar el mensaje r del usuario u y 
%devuelve el mensaje de respuesta result para el 
%usuario. En el contexto de este problema, es necesario que el contenido del
%mensaje r no se corresponda con ning’un comando del gateway g. 
%Primero se debe determinar si el mensaje r posee alguna keyword definida para
%poder determinar  la trivia a la que el usuario quiere jugar. En caso de no
%poder determinar ninguna trivia, el mensaje de respuesta deber’a decir: ''No te
%entiendo.'' Una vez determinada la trivia, el mensaje de respuesta depender’a
%del procesamiento que la trivia le realice al mensaje r seg’un el usuario u sea
%o no sea jugador actualmente. Considerar los problemas registrarJugadorT y procesarRespuestaT.

\begin{problema}{procesarMensajeG}{g: Gateway, u: Usuario, r: SMS}{SMS}
	\requiere[noEsComando]{damePalabras(texto(r))_0 \not\in comandos(g)}
	\requiere[numeroValido]{nroDestino(r) == numero(g)}
	
	\medskip
	
	\modifica{g}
	
	\medskip
	\asegura{procesarMensajesAux(g,pre(g),u,r,result)}
	
\end{problema}

\medskip

\begin{aux}{procesarMensajesAux}{g,preg: Gateway, u: Usuario, r,result:SMS}{Bool}{\\
loDemasNoCambiaG(g,preg) \\
\ylogico nroDestino(result) == u \\
\ylogico invalido(preg,r,result) \\
\ylogico esta(g,preg,u,r,result) \\
\ylogico noEsta(g,preg,u,r,result) \\
\ylogico restoIguales(g,preg,r)	
}
\end{aux}

\medskip

\begin{aux}{invalido}{preg: Gateway, r,result:SMS}{Bool}{\\
((\not\exists h \selec trivias(preg))damePalabras(texto(r))_0 \in keywords(h))
\implica texto(result) == ''No\ te\ entiendo.''
} 
\end{aux}

\medskip

\begin{aux}{esta}{g,preg: Gateway, u:Usuario, r,result:SMS}{Bool}{\\
((\exists h \selec trivias(preg)) damePalabras(texto(r))_0 
\in keywords(h) \ylogico u \in participantes(h)) \implica \\
(((\exists j \selec trivias(g))damePalabras(texto(r)_0) \in keywords(j))
\ylogico \\ procesarRespuestaAux(j,h,u,texto(r), result ))
}
\end{aux}

\medskip

\begin{aux}{noEsta}{g,preg: Gateway, u:Usuario, r,result:SMS}{Bool}{\\
((\exists h \selec trivias(preg)) damePalabras(texto(r))_0 
\in keywords(h) \ylogico u \notin participantes(h)) \implica \\
(((\exists j \selec trivias(g))damePalabras(texto(r)_0) \in keywords(j))
\ylogico \\ registrarJugadorAux(j,h,u,result))
}
\end{aux}

\medskip

\begin{aux}{restoIguales}{g,preg: Gateway,r:SMS}{Bool}{\\
(\longitud{trivias(preg)} == \longitud{trivias(g)}) \\
\ylogico (\forall h \selec trivias(preg), damePalabras(texto(r))_0 \not\in keywords(h))\\
(\exists t \selec trivias(g)) h == t
}
\end{aux}

% Arpobado por Lea Lunes 26 de Septiembre. Cambi� un par de cosas para tener en
% cuenta, despu�s comparen con el anterior. Tambi�n est�n verificados los
% par�ntesis, as� que revisen bien antes de cambiar alguno !
				


